Termination w.r.t. Q proof of /tmp/tmpGwJFPU/z083.srs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

b(d(b(x1))) → c(d(b(x1)))
b(a(c(x1))) → b(c(x1))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))

Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

b(d(b(x1))) → c(d(b(x1)))
b(a(c(x1))) → b(c(x1))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

b(d(b(x1))) → c(d(b(x1)))
b(a(c(x1))) → b(c(x1))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

b(a(c(x1))) → b(c(x1))

Used ordering:
Polynomial interpretation [25]:

POL(a(x₁)) = 1 + x₁
POL(b(x₁)) = 1 + x₁
POL(c(x₁)) = 1 + x₁
POL(d(x₁)) = x₁

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

b(d(b(x1))) → c(d(b(x1)))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

B(b(b(x1))) → B(c(x1))
D(c(x1)) → B(d(x1))
B(b(b(x1))) → A(b(c(x1)))
D(a(c(x1))) → B(x1)
A(d(x1)) → D(c(x1))
D(c(x1)) → D(b(d(x1)))
D(c(x1)) → D(x1)
D(a(c(x1))) → B(b(x1))

The TRS R consists of the following rules:

b(d(b(x1))) → c(d(b(x1)))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

B(b(b(x1))) → B(c(x1))
D(c(x1)) → B(d(x1))
B(b(b(x1))) → A(b(c(x1)))
D(a(c(x1))) → B(x1)
A(d(x1)) → D(c(x1))
D(c(x1)) → D(b(d(x1)))
D(c(x1)) → D(x1)
D(a(c(x1))) → B(b(x1))

The TRS R consists of the following rules:

b(d(b(x1))) → c(d(b(x1)))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 6 less nodes.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

              ↳ UsableRulesProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

D(c(x1)) → D(b(d(x1)))
D(c(x1)) → D(x1)

The TRS R consists of the following rules:

b(d(b(x1))) → c(d(b(x1)))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

              ↳ UsableRulesProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

D(c(x1)) → D(b(d(x1)))
D(c(x1)) → D(x1)

The TRS R consists of the following rules:

d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

D(c(x1)) → D(b(d(x1)))
D(c(x1)) → D(x1)

The TRS R consists of the following rules:

d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

D(c(x1)) → D(x1)

Used ordering: POLO with Polynomial interpretation [25]:

POL(D(x₁)) = x₁
POL(a(x₁)) = 2 + x₁
POL(b(x₁)) = 2 + x₁
POL(c(x₁)) = 2 + x₁
POL(d(x₁)) = x₁

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ Narrowing

  ↳ QTRS Reverse

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

D(c(x1)) → D(b(d(x1)))

The TRS R consists of the following rules:

d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule D(c(x1)) → D(b(d(x1))) at position [0] we obtained the following new rules:

D(c(a(c(x0)))) → D(b(b(b(x0))))
D(c(b(x0))) → D(c(d(b(x0))))
D(c(c(x0))) → D(b(d(b(d(x0)))))
D(c(c(x0))) → D(b(b(d(x0))))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ Narrowing

  ↳ QTRS Reverse

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

D(c(c(x0))) → D(b(b(d(x0))))
D(c(c(x0))) → D(b(d(b(d(x0)))))
D(c(a(c(x0)))) → D(b(b(b(x0))))
D(c(b(x0))) → D(c(d(b(x0))))

The TRS R consists of the following rules:

d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule D(c(a(c(x0)))) → D(b(b(b(x0)))) at position [0] we obtained the following new rules:

D(c(a(c(b(b(x0)))))) → D(b(b(a(b(c(x0))))))
D(c(a(c(d(b(x0)))))) → D(b(b(c(d(b(x0))))))
D(c(a(c(b(x0))))) → D(b(a(b(c(x0)))))
D(c(a(c(x0)))) → D(a(b(c(x0))))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ DependencyGraphProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

D(c(a(c(b(x0))))) → D(b(a(b(c(x0)))))
D(c(a(c(b(b(x0)))))) → D(b(b(a(b(c(x0))))))
D(c(a(c(x0)))) → D(a(b(c(x0))))
D(c(c(x0))) → D(b(d(b(d(x0)))))
D(c(c(x0))) → D(b(b(d(x0))))
D(c(a(c(d(b(x0)))))) → D(b(b(c(d(b(x0))))))
D(c(b(x0))) → D(c(d(b(x0))))

The TRS R consists of the following rules:

d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ DependencyGraphProof

                                ↳ QDP

                                  ↳ QDPToSRSProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

D(c(c(x0))) → D(b(b(d(x0))))
D(c(c(x0))) → D(b(d(b(d(x0)))))
D(c(b(x0))) → D(c(d(b(x0))))

The TRS R consists of the following rules:

d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The finiteness of this DP problem is implied by strong termination of a SRS due to [12].

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ DependencyGraphProof

                                ↳ QDP

                                  ↳ QDPToSRSProof

                                    ↳ QTRS

                                      ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))
D(c(c(x0))) → D(b(b(d(x0))))
D(c(c(x0))) → D(b(d(b(d(x0)))))
D(c(b(x0))) → D(c(d(b(x0))))

Q is empty.

We have reversed the following QTRS:
The set of rules R is

d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))
D(c(c(x0))) → D(b(b(d(x0))))
D(c(c(x0))) → D(b(d(b(d(x0)))))
D(c(b(x0))) → D(c(d(b(x0))))

The set Q is empty.
We have obtained the following QTRS:

c(d(x)) → d(b(x))
c(d(x)) → d(b(d(x)))
c(a(d(x))) → b(b(x))
b(d(b(x))) → b(d(c(x)))
b(b(b(x))) → c(b(a(x)))
c(c(D(x))) → d(b(b(D(x))))
c(c(D(x))) → d(b(d(b(D(x)))))
b(c(D(x))) → b(d(c(D(x))))

The set Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ DependencyGraphProof

                                ↳ QDP

                                  ↳ QDPToSRSProof

                                    ↳ QTRS

                                      ↳ QTRS Reverse

                                        ↳ QTRS

                                          ↳ RFCMatchBoundsTRSProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

c(d(x)) → d(b(x))
c(d(x)) → d(b(d(x)))
c(a(d(x))) → b(b(x))
b(d(b(x))) → b(d(c(x)))
b(b(b(x))) → c(b(a(x)))
c(c(D(x))) → d(b(b(D(x))))
c(c(D(x))) → d(b(d(b(D(x)))))
b(c(D(x))) → b(d(c(D(x))))

Q is empty.

Termination of the TRS R could be shown with a Match Bound [6,7] of 2. This implies Q-termination of R.
The following rules were used to construct the certificate:

c(d(x)) → d(b(x))
c(d(x)) → d(b(d(x)))
c(a(d(x))) → b(b(x))
b(d(b(x))) → b(d(c(x)))
b(b(b(x))) → c(b(a(x)))
c(c(D(x))) → d(b(b(D(x))))
c(c(D(x))) → d(b(d(b(D(x)))))
b(c(D(x))) → b(d(c(D(x))))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

1380, 1381, 1382, 1383, 1384, 1386, 1387, 1385, 1388, 1389, 1392, 1393, 1390, 1391, 1394, 1395, 1396, 1397, 1398, 1400, 1401, 1399, 1402, 1405, 1406, 1403, 1404, 1407, 1408, 1409, 1410, 1411, 1412, 1413, 1414, 1415

Node 1380 is start node and node 1381 is final node.

Those nodes are connect through the following edges:

1380 to 1382 labelled b_1(0), d_1(0)
1380 to 1385 labelled d_1(0)
1380 to 1388 labelled c_1(0)
1380 to 1390 labelled d_1(0)
1380 to 1397 labelled c_1(1)
1380 to 1412 labelled b_1(1)
1381 to 1381 labelled #_1(0), d_1(1), d_1(2)
1382 to 1383 labelled d_1(0)
1382 to 1381 labelled b_1(0)
1382 to 1394 labelled b_1(1)
1382 to 1397 labelled c_1(1)
1382 to 1414 labelled b_1(2)
1383 to 1384 labelled c_1(0)
1383 to 1381 labelled c_1(0)
1383 to 1399 labelled d_1(1)
1383 to 1402 labelled b_1(1), d_1(1)
1383 to 1403 labelled d_1(1)
1383 to 1397 labelled c_1(1)
1384 to 1381 labelled D_1(0)
1386 to 1387 labelled b_1(0)
1386 to 1381 labelled d_1(0)
1387 to 1381 labelled D_1(0)
1385 to 1386 labelled b_1(0)
1385 to 1394 labelled b_1(1)
1385 to 1414 labelled b_1(2)
1388 to 1389 labelled b_1(0)
1389 to 1381 labelled a_1(0)
1392 to 1393 labelled b_1(0)
1393 to 1381 labelled D_1(0)
1390 to 1391 labelled b_1(0)
1390 to 1407 labelled b_1(1)
1391 to 1392 labelled d_1(0)
1394 to 1395 labelled d_1(1)
1395 to 1396 labelled c_1(1)
1395 to 1381 labelled c_1(1)
1395 to 1399 labelled d_1(1)
1395 to 1402 labelled b_1(1), d_1(1)
1395 to 1403 labelled d_1(1)
1395 to 1409 labelled d_1(2)
1395 to 1397 labelled c_1(1)
1396 to 1381 labelled D_1(1)
1397 to 1398 labelled b_1(1)
1398 to 1381 labelled a_1(1)
1400 to 1401 labelled b_1(1)
1401 to 1381 labelled D_1(1)
1399 to 1400 labelled b_1(1)
1402 to 1381 labelled b_1(1)
1402 to 1394 labelled b_1(1)
1402 to 1397 labelled c_1(1)
1402 to 1414 labelled b_1(2)
1405 to 1406 labelled b_1(1)
1406 to 1381 labelled D_1(1)
1403 to 1404 labelled b_1(1)
1403 to 1410 labelled b_1(2)
1404 to 1405 labelled d_1(1)
1407 to 1408 labelled d_1(1)
1408 to 1393 labelled c_1(1)
1409 to 1381 labelled b_1(2)
1409 to 1394 labelled b_1(1)
1409 to 1397 labelled c_1(1)
1409 to 1414 labelled b_1(2)
1410 to 1411 labelled d_1(2)
1411 to 1406 labelled c_1(2)
1412 to 1413 labelled d_1(1)
1413 to 1402 labelled c_1(1)
1414 to 1415 labelled d_1(2)
1415 to 1402 labelled c_1(2)

We have reversed the following QTRS:
The set of rules R is

b(d(b(x1))) → c(d(b(x1)))
b(a(c(x1))) → b(c(x1))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))

The set Q is empty.
We have obtained the following QTRS:

b(d(b(x))) → b(d(c(x)))
c(a(b(x))) → c(b(x))
d(a(x)) → c(d(x))
b(b(b(x))) → c(b(a(x)))
c(d(x)) → d(b(x))
c(d(x)) → d(b(d(x)))
c(a(d(x))) → b(b(x))

The set Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

  ↳ QTRS Reverse

    ↳ QTRS

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

b(d(b(x))) → b(d(c(x)))
c(a(b(x))) → c(b(x))
d(a(x)) → c(d(x))
b(b(b(x))) → c(b(a(x)))
c(d(x)) → d(b(x))
c(d(x)) → d(b(d(x)))
c(a(d(x))) → b(b(x))

Q is empty.

We have reversed the following QTRS:
The set of rules R is

b(d(b(x1))) → c(d(b(x1)))
b(a(c(x1))) → b(c(x1))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))

The set Q is empty.
We have obtained the following QTRS:

b(d(b(x))) → b(d(c(x)))
c(a(b(x))) → c(b(x))
d(a(x)) → c(d(x))
b(b(b(x))) → c(b(a(x)))
c(d(x)) → d(b(x))
c(d(x)) → d(b(d(x)))
c(a(d(x))) → b(b(x))

The set Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

    ↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

b(d(b(x))) → b(d(c(x)))
c(a(b(x))) → c(b(x))
d(a(x)) → c(d(x))
b(b(b(x))) → c(b(a(x)))
c(d(x)) → d(b(x))
c(d(x)) → d(b(d(x)))
c(a(d(x))) → b(b(x))

Q is empty.